Hochleistungs-Termersetzung

Projektleitung und Mitarbeiter

Bündgen, R. (Dr. rer. nat., Arbeitsbereich Computer-Algebra), Göbel, M. (Dipl. Inform.), Küchlin, W. (Prof. Dr. sc. techn.)

Mittelgeber : DFG

Forschungsbericht : 1994-1996

Tel./ Fax.:

Projektbeschreibung

Das bestehende sequentielle Termersetzungssystem ReDuX wird zum parallelen System PaReDuX weiterentwickelt. PaReDuX enthält verschiedene Beweismethoden der Termersetzung wie Knuth-Bendix Vervollständigung, AC-Vervollständigung, nicht abbrechende Vervollständigung und induktive Vervollständigung. Diese Methoden werden in Theorie und Praxis so parallelisiert, daß sie signifikant schneller werden. PaReDuX wird auf die Verifikation von Schaltungsentwürfen wie z. B. Mikroprozessoren angewendet. PaReDuX benutzt die Systemumgebung von PARSAC auf einem Netz von parallelen Arbeitsplatzrechnern.

Publikationen

Bündgen, R., Göbel, M., Küchlin, W.: Parallel ReDuX -> PaReDuX. Proc. RTA-95, LNCS 914, Springer-Verlag 1995.

INDEX HOME SUCHEN KONTAKT LINKS

qvf-info@uni-tuebingen.de(qvf-info@uni-tuebingen.de) - Stand: 30.11.96
Copyright Hinweise